Code verification and validation is the process of determining that a software program meets all specifications and fulfills its intended purpose. Code verification addresses the issue of the software program achieving its goals without any bugs or gaps. On the other hand, code validation ascertains whether or not the software meets high-level requirements and addresses the problem to be solved. Code verification ensures that “you built it right”. Code validation ensures that “you built the right thing”.
Static program analysis refers to analyzing computer software without actually executing the software. Static program analysis has been shown to be of great value in automating code verification tasks. Examples include functional verification tools such as Coverity™, as well as security analysis tools such as IBM Security AppScan Source Edition™ and HP Fortify 360™. One challenge faced by all tools based upon static program analysis is to achieve a proper balance between accuracy and scalability. These two considerations are in conflict. Precision is achieved by building a granular albeit expensive analysis model. Scalability requires the opposite—a lightweight and less descriptive model.
Various analysis specialization techniques have been developed in an attempt to address the inherent tradeoff between accuracy and scalability. One set of techniques provides specialization for certain forms of static analysis according to one or more concrete runs of the program. Another approach applies randomized algorithms inspired by a theory called machine learning. Yet another approach, termed Counter-Example Guided Abstraction Refinement (CEGAR) refines an abstraction guided by false counterexample traces. All three of the foregoing techniques may potentially improve the ability of the static program analysis procedure to scale while remaining precise. The specialization process, however, is expensive and requires its own set of non-trivial analyses. Thus, there exists a need to overcome at least one of the preceding deficiencies and limitations of the related art.